Nuprl Lemma : lt_to_le_rw
12,41
postcript
pdf
i
,
j
:
. {(
i
<
j
)
((
i
+1)
j
)}
latex
ProofTree
Definitions
{
T
}
Lemmas
lt
to
le
origin
i, j:
. {(i < j) 
((i+1) 
j)}
i, j:. {(i < j) ((i+1) j)}